Termination Proof Script
Consider the TRS R consisting of the rewrite rules
1:
app
(
app
(
app
(
comp
,f),g),x)
→
app
(f,
app
(g,x))
2:
app
(
twice
,f)
→
app
(
app
(
comp
,f),f)
There are 4 dependency pairs:
3:
APP
(
app
(
app
(
comp
,f),g),x)
→
APP
(f,
app
(g,x))
4:
APP
(
app
(
app
(
comp
,f),g),x)
→
APP
(g,x)
5:
APP
(
twice
,f)
→
APP
(
app
(
comp
,f),f)
6:
APP
(
twice
,f)
→
APP
(
comp
,f)
The approximated dependency graph contains one SCC: {3-5}.
Consider the SCC {3-5}.
The constraints could not be solved.
Tyrolean Termination Tool
(0.01 seconds) --- May 3, 2006